DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2023.19

Synchronized CTL over One-Counter Automata

Authors: Shaull Almagor, Daniel Assa, and Udi Boker

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract

We consider the model-checking problem of Synchronized Computation-Tree Logic (CTL+Sync) over One-Counter Automata (OCAs). CTL+Sync augments CTL with temporal operators that require several paths to satisfy properties in a synchronous manner, e.g., the property "all paths should eventually see p at the same time". The model-checking problem for CTL+Sync over finite-state Kripke structures was shown to be in 𝖯^{NP^NP}. OCAs are labelled transition systems equipped with a non-negative counter that can be zero-tested. Thus, they induce infinite-state systems whose computation trees are not regular. The model-checking problem for CTL over OCAs was shown to be PSPACE-complete. We show that the model-checking problem for CTL+Sync over OCAs is decidable. However, the upper bound we give is non-elementary. We therefore proceed to study the problem for a central fragment of CTL+Sync, extending CTL with operators that require all paths to satisfy properties in a synchronous manner, and show that it is in EXP^NEXP (and in particular in EXPSPACE), by exhibiting a certain "segmented periodicity" in the computation trees of OCAs.

Cite as

Shaull Almagor, Daniel Assa, and Udi Boker. Synchronized CTL over One-Counter Automata. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.FSTTCS.2023.19,
  author =	{Almagor, Shaull and Assa, Daniel and Boker, Udi},
  title =	{{Synchronized CTL over One-Counter Automata}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.19},
  URN =		{urn:nbn:de:0030-drops-193921},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.19},
  annote =	{Keywords: CTL, Synchronization, One Counter Automata, Model Checking}
}

Search Results

Documents authored by Assa, Daniel

Synchronized CTL over One-Counter Automata

Abstract

Cite as

Thanks for your feedback!

Could not send message